$\forall$$T$:Type, $r$, ${\it r'}$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$). ($r$ $\Lleftarrow\!\Rrightarrow$\{$T$\} ${\it r'}$) $\Rightarrow$ (${\it r'}$ $\Lleftarrow\!\Rrightarrow$\{$T$\} $r$)